#if !defined(BytecodeHeader)
#define BytecodeHeader

#include <set>
#include <vector>

class Node;
class pNode;
class ProverFactoryBase;
class Serializer;
class Snippet;

enum Instruction {
  BIND_____, // Creates a new binder into stack top and bind two variables.
  BINDUNDO_, // Un-binds the top binder in stack and removes it.
  CALL_____, // Invokes a subroutine.
  CUT______, // Actuates a cut and remove all provers after last cut point.
  CUTFAIL__, // Fails to a cut point; un-bind and jumps to fail point.
  CUTPOINT_, // Store machine states for a given cut point.
  EXEC_____, // Interprets the structure of variable once.
  FAIL_____, // Ends running the byte-code stream and fail ultimately.
  JUMP_____, // Initiates a jump; switches instruction pointer to somewhere else.
  JUMPFAIL_, // Initiates a jump if the previous BIND or PROVER.TRY failed.
  NEWREF___, // Set a variable to a new, unbounded reference.
  PROVEN___, // Solution found, but may backtrack to next instruction.
  PROVERBCD, // Creates prover for a byte-code stream.
  PROVERPOP, // Removes the top prover.
  PROVERPRO, // Creates prover that is limited by a prototype (not variable).
  PROVERPSH, // Creates prover to prove structure of variable into stack top.
  PROVERSYS, // Creates prover for a system predicate.
  PROVERTRY, // Tries to attempt the prover at stack-top.
  RETURN___, // Returns from subroutine.
  SETCONST_, // Sets a variable to a constant structure.
  SETTOPROV, // Sets a variable to the proving target.
  SETVAR___, // Sets a variable according to another variable.
  TUPLEAPP_, // Appends the structure of variable to tuple.
  TUPLEFROM, // Gets a tuple from a variable.
  TUPLENEW_, // Creates a tuple with suggested length (can extend beyond).
  TUPLENTH_, // Grabs the n-th element of a tuple to a variable.
  TREELR___, // Assigns the structures in variables to left/right nodes.
  TREEOP___
// Forms a tree with specified operator.
};

struct Bytecode { // Packs neatly to 8 bytes in i386 architecture
  short instruction;
  union {
    short var;
  } o1;
  union {
    int n;
    char op[2];
    Node *constant;
    ProverFactoryBase *systemProverFactory;
    Snippet *snippet;
  } o2;
};

struct Snippet {
  Snippet () :
    valid (true), nVariables (0), toProveVariable (0), nCutPoints (0) {
  }

  void invalidate () {
    if(valid) {
      valid = false;
      for(std::set<Snippet*>::iterator iter = cascadeInvalidates.begin (); iter
          != cascadeInvalidates.end (); iter++)
        (*iter)->invalidate ();
    }
    cascadeNodes.clear ();
  }

  // Serialization
  // How to serialize cascade relations?
  void serialize (const Serializer&);

  bool valid;
  int nVariables, toProveVariable, nCutPoints;
  std::vector<Bytecode> codes;

  // Maintaining link to others and facilitate cascaded invalidation/deletion
  std::set<Snippet*> cascadeInvalidates;
  std::set<pNode> cascadeNodes;
};

// Cannot be included earlier. Recursive header problems.
#include "bind.h"
#include "prototype.h"
#include "prover.h"
#include "system.h"

class Prover;

class BytecodeExecutor : public Prover {
public:
  BytecodeExecutor (Snippet &s, Node &n, System &sys) :
    snippet (s), toProve (n), system (sys), ip (snippet.codes.begin ()),
        locals (s.nVariables), cutPoints (snippet.nCutPoints), result (true) {
  }
  ~BytecodeExecutor ();

  bool prove ();

  Snippet &snippet;
  Node &toProve;
  System &system;

  typedef std::vector<Bytecode>::iterator Ip;
  Ip ip; // Instruction pointer

  // Local register storage
  std::vector<pNode> locals;

  // Stack for bindings we have done
  std::vector<Binder> binders;

  // Stack for calling subroutines
  std::vector<Ip> callees;

  // Paired-stack for interpreted provers
  std::vector<Prover*> provers;

  struct CutPoint {
    Trail::Pointer trailPointer;
    unsigned int binderIndex;
    unsigned int calleeIndex;
    unsigned int proverIndex;
  };
  std::vector<CutPoint> cutPoints;

  Tuple *tuple;
  Node *left, *right;
  Binder binder;

  bool result;
};

class System;

bool compileExecuteBytecode (Prototype&, Snippet&, System&);

#endif
